| Definitions | list-diff(eq; as; bs), ecl-add-catch(A; l), ecl-add-throw(A; m), add-ecl-act(A; m), compat(T; l1; l2), ecl-trans-act(ds; da; A), ecl-trans-tuple{i:l}(ds; da), reset-ecl-tuple(A), ge(i; j), l_exists(L; T; x.P(x)), int_seg(i; j), lelt(i; j; k), combine-ecl-tuples2(A; B; f; g), isl(x), outl(x), ||as||, ecl-trans-a(v), ecl-trans-ks(v), ecl-trans-state(v; L), ecl-trans-init(v),  T, t.2, iseg(T; l1; l2), ecl-trans-es(v), combine-ecl-tuples(A; B; f; g), ecl-act(ds; da; m; x), Knd, (x  l), P  Q, l_all(L; T; x.P(x)), True, ecl-halt(ds; da; x), spreadn(a; x,y,z.t(x;y;z)), event-info(ds;da), ma-valtype(da; k),   x,y. t(x;y), list_accum(x,a.f(x;a); y; l), bor(p; q), ecl-trans-state-from(v; z; L), reduce(f; k; as), tt, deq-member(eq; x; L), Y, t.1, ecl-trans-type(A), sq_type(T), top, guard(T), ecl-trans-h(v), ecl-trans-halt2(ds; da; A), ecl-trans-normal(x), ff,  A, spreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), ecl-trans(x), sorted(L), A c B,  , ecl-base-tuple(k; test), if b then t else f fi , band(p; q),  , False, A  B,  b, P   Q, P  Q, t T, P Q, x. t(x), prop{i:l},  x:A. B(x),  x:A. B(x), P Q, subtype(S; T), hd(l), tl(l), append(as; bs), decl-state(ds), null(as), decidable(P), x(s1,s2), Unit,  , x(s), eq_knd(a; b),  |
| Lemmas | ecl-trans-halt2-add-catch, member-list-diff, ecl-add-catch wf, no repeats filter, sorted-filter, nat-deq wf, decidable equal nat, member-s-insert, ecl-add-throw wf, ecl-trans-halt2-add-throw, s-insert-no-repeats, s-insert-sorted, list accum wf, iseg-transition-lemma, add-ecl-act wf, ecl-reset-lemma, ecl-reset-state, ecl-trans-init wf, hd wf, tl wf, general-append-cancellation, ecl-trans-act-functionality2, append nil sq, ecl-reset-init, length append, ecl-trans-act functionality, decidable false, assert of null, iseg length, non neg length, star-append wf, star-append-iff, ecl-reset-halt, reset-ecl-tuple wf, bool cases, ge wf, nat properties, l exists reduce, append-impossible2, reduce wf, iseg append single, l exists wf, decidable lt, decidable int equal, it wf, ecl-normal-combine2, unit wf, ifthenelse wf, combine-ecl-trans-state2, combine-ecl-tuples2 wf, append-impossible, cons one one, append assoc, append-cancellation-right, append-cancellation, assert-deq-member, deq-member wf, iseg antisymmetry, iseg append, ecl-act-halt, member append, ecl-halt-nil, append is nil, ecl-trans-a wf, decl-state wf, ecl-trans-act-last, ecl-trans-act-nil, ecl-trans-ks wf, iseg weakening, append iseg, pi1 wf, pi2 wf, decidable functionality, combine-ecl-trans-state0, true wf, squash wf, iseg transitivity, common iseg compat, ecl-halt-unique, combine-ecl-trans-state1, member-merge, ecl-normal-combine, bfalse wf, assert of lt int, iff functionality wrt iff, combine-ecl-tuples wf, all functionality wrt iff, lt int wf, ecl-trans-tuple wf, IdLnk wf, l all nil, l all cons, assert of bor, or functionality wrt iff, l all append, nil member, ecl-base-tuple wf, length-append, length wf1, iseg append0, bor wf, last lemma, Kind-deq wf, ma-valtype wf, last wf, fpf-cap wf, append wf, l all wf2, null wf3, first-iseg, decidable assert, Knd sq, bool wf, eclbase wf, last induction, list accum append, ecl-trans-h wf, ecl-trans-state-from wf, not wf, member wf, length wf nat, assert-eq-knd, eqff to assert, assert of bnot, bnot wf, eqtt to assert, eq knd wf, not functionality wrt iff, subtype rel self, ecl-trans-state-append, btrue wf, top wf, bool sq, assert of band, band wf, ecl-trans-state wf, ecl-trans-type wf, eq int wf, assert wf, iff transitivity, implies functionality wrt iff, assert of eq int, and functionality wrt iff, select wf, le wf, finite-type-bool, int seg wf, length wf2, false wf, decidable equal bool, no repeats nil, ecl-induction, nat plus inc, ecl-trans-halt2 wf, ecl-halt wf, nat plus wf, ecl-trans wf, nat wf, ecl wf, fpf wf, ecl-act wf, event-info wf, Id wf, l member wf, ecl-trans-normal wf, ecl-trans-es wf, Knd wf, ecl-trans-act wf, iff wf, iseg wf |
(